import LeanProject.Short

/-- 我们称序列 `u` 收敛到极限 `l`，如果以下成立。-/
def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε


/-
## 子序列
我们现在将玩子序列。
我们称 `φ : ℕ → ℕ` 是一个提取，若它是（严格）递增的。
-/

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

/-- 我们称实数 `a` 是序列 `u` 的聚点，若 `u` 有一个收敛到 `a` 的子序列。-/
def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a

/-- 如果 `u` 趋于 `l`，那么它的所有聚点都等于 `l`。-/
lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l := by
  apply eq_of_abs_sub_le_all
  intro ε εpos
  simp [seq_limit] at hl
  rcases hl (ε/2) (by exact half_pos εpos) with ⟨N1, hu⟩
  simp [cluster_point] at ha
  rcases ha with ⟨φ, ⟨hph, huph⟩⟩
  simp [seq_limit] at huph
  rcases huph (ε/2) (by exact half_pos εpos) with ⟨N2, ha⟩
  let mN := max N1 N2
  have hmN: φ mN ≥ N1 := by
    calc
      φ mN ≥ mN := by apply id_le_extraction' hph mN
      _ ≥ N1 := by exact Nat.le_max_left N1 N2
  rcases hu (φ mN) hmN with h1
  rcases ha mN (Nat.le_max_right N1 N2) with h2
  calc
    |a - l| ≤ |a - u (φ mN)| + |u (φ mN) - l| := by apply abs_sub_le
    _ = |u (φ mN) - a| + |u (φ mN) - l|:= by rw [abs_sub_comm]
    _ ≤ ε / 2 + ε / 2 := by gcongr
    _ = ε := by ring
  
#check cluster_limit